<html>
<head><meta charset="utf-8"><title>Specification Challenge · wg-formal-methods · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/index.html">wg-formal-methods</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Specification.20Challenge.html">Specification Challenge</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="246130002"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Specification%20Challenge/near/246130002" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Specification.20Challenge.html#246130002">(Jul 15 2021 at 17:41)</a>:</h4>
<p>The idea of the specification challenge is to explore the specifications of short Rust programs, and discuss syntax and semantics of a specification language for Rust.<br>
Participants submit short programs and also <em>specify</em> the programs of others in the syntax of their choice.</p>
<p>Currently I think this should be open until September, though we'll adjust as need arises.</p>
<h1>Program Submission Format</h1>
<p>Submissions should be posted as replies to this narrow.</p>
<ul>
<li>Submissions should be short (10 line maximum) programs with at least one clearly named function that should be specified. </li>
<li>Submitted programs may use any language feature of Rust (traits, unsafe, etc).  </li>
<li>Each submission should be accompanied by an informal description of the desired specification. </li>
<li>Submissions should have no specifications themselves, this is to avoid influencing others. </li>
</ul>
<p>Example:</p>
<div class="codehilite" data-code-language="Rust"><pre><span></span><code><span class="c1">// The result should be the sum of the inputs</span>
<span class="k">fn</span> <span class="nf">addition</span><span class="p">(</span><span class="n">x</span>: <span class="kt">u32</span><span class="p">,</span><span class="w"> </span><span class="n">y</span>: <span class="kt">u32</span><span class="p">)</span><span class="w"> </span>-&gt; <span class="kt">u32</span> <span class="p">{</span><span class="w"></span>
<span class="w">    </span><span class="n">x</span><span class="w"> </span><span class="o">+</span><span class="w"> </span><span class="n">y</span><span class="w"></span>
<span class="p">}</span><span class="w"></span>
</code></pre></div>
<h1>Specification Submission Format</h1>
<p>Participants are strongly encouraged to specify the programs of others, using the syntax of their choosing. If your specifications use an uncommon construct, please add a few lines of explanation.</p>
<ul>
<li>Submissions should be an annotated version of the specified program, please don't only submit the specification itself. </li>
<li>Specified programs should be DMed or emailed (<a href="mailto:xldenis@lri.fr">xldenis@lri.fr</a>) to me, at the end of the 'challenge' they will be published. </li>
</ul>
<p>Example:</p>
<div class="codehilite" data-code-language="Rust"><pre><span></span><code><span class="c1">// The `result` keyword refers to the return value of the function.</span>
<span class="c1">// Addition in the specification is unbounded (ie not machine addition).</span>
<span class="cp">#[ensures(result == x + y)]</span><span class="w"></span>
<span class="k">fn</span> <span class="nf">addition</span><span class="p">(</span><span class="n">x</span>: <span class="kt">u32</span><span class="p">,</span><span class="w"> </span><span class="n">y</span>: <span class="kt">u32</span><span class="p">)</span><span class="w"> </span>-&gt; <span class="kt">u32</span> <span class="p">{</span><span class="w"></span>
<span class="w">    </span><span class="n">x</span><span class="w"> </span><span class="o">+</span><span class="w"> </span><span class="n">y</span><span class="w"></span>
<span class="p">}</span><span class="w"></span>
</code></pre></div>



<a name="246130333"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Specification%20Challenge/near/246130333" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Specification.20Challenge.html#246130333">(Jul 15 2021 at 17:44)</a>:</h4>
<h1>Entry 1</h1>
<div class="codehilite" data-code-language="Rust"><pre><span></span><code><span class="c1">// The return value should be the mutable reference being pointed to by the parameter `x`.</span>
<span class="c1">// Ideally submitted specifications should also explain how pointers are modeled / handled</span>
<span class="c1">// their specification (ie how you link the return value to `x`)</span>
<span class="k">fn</span> <span class="nf">unnest</span><span class="o">&lt;'</span><span class="na">a</span><span class="p">,</span><span class="w"> </span><span class="o">'</span><span class="na">b</span><span class="w"> </span>: <span class="o">'</span><span class="na">a</span><span class="o">&gt;</span><span class="p">(</span><span class="n">x</span><span class="w"> </span>: <span class="kp">&amp;</span><span class="o">'</span><span class="na">a</span> <span class="nc">mut</span><span class="w"> </span><span class="o">&amp;'</span><span class="na">b</span><span class="w"> </span><span class="k">mut</span><span class="w"> </span><span class="kt">u32</span><span class="p">)</span><span class="w"> </span>-&gt; <span class="kp">&amp;</span><span class="o">'</span><span class="na">a</span> <span class="nc">mut</span><span class="w"> </span><span class="kt">u32</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">  </span><span class="o">*</span><span class="w"> </span><span class="n">x</span><span class="w"></span>
<span class="p">}</span><span class="w"></span>
</code></pre></div>



<a name="246130764"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Specification%20Challenge/near/246130764" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Specification.20Challenge.html#246130764">(Jul 15 2021 at 17:47)</a>:</h4>
<h1>Entry 2</h1>
<div class="codehilite" data-code-language="Rust"><pre><span></span><code><span class="c1">// All implementors of Add should be be a group:</span>
<span class="c1">//  - have 0 as identity (which means being able to define a 0)</span>
<span class="c1">//      ie: `x.add(Self::zero()) == x`</span>
<span class="c1">//  - be commutative: `x.add(y) == y.add(x)`</span>
<span class="c1">//  - be associative: x.add(y.add(z)) == (x.add(y)).add(z)</span>
<span class="k">pub</span><span class="w"> </span><span class="k">trait</span><span class="w"> </span><span class="n">Add</span><span class="o">&lt;</span><span class="n">Rhs</span><span class="w"> </span><span class="o">=</span><span class="w"> </span><span class="bp">Self</span><span class="o">&gt;</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">    </span><span class="k">type</span> <span class="nc">Output</span><span class="p">;</span><span class="w"></span>
<span class="w">    </span><span class="cp">#[must_use]</span><span class="w"></span>
<span class="w">    </span><span class="k">pub</span><span class="w"> </span><span class="k">fn</span> <span class="nf">add</span><span class="p">(</span><span class="bp">self</span><span class="p">,</span><span class="w"> </span><span class="n">rhs</span>: <span class="nc">Rhs</span><span class="p">)</span><span class="w"> </span>-&gt; <span class="nc">Self</span>::<span class="n">Output</span><span class="p">;</span><span class="w"></span>
<span class="p">}</span><span class="w"></span>
</code></pre></div>



<a name="246131330"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Specification%20Challenge/near/246131330" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Specification.20Challenge.html#246131330">(Jul 15 2021 at 17:51)</a>:</h4>
<h1>Entry 3</h1>
<div class="codehilite" data-code-language="Rust"><pre><span></span><code><span class="c1">// The returned reference should be the greater of the two input references</span>
<span class="k">fn</span> <span class="nf">max_of</span><span class="o">&lt;'</span><span class="na">a</span><span class="o">&gt;</span><span class="p">(</span><span class="n">a</span>: <span class="kp">&amp;</span><span class="o">'</span><span class="na">a</span> <span class="nc">mut</span><span class="w"> </span><span class="kt">u32</span><span class="p">,</span><span class="w"> </span><span class="n">b</span>: <span class="kp">&amp;</span><span class="o">'</span><span class="na">a</span> <span class="nc">mut</span><span class="w"> </span><span class="kt">u32</span><span class="p">)</span><span class="w"> </span>-&gt; <span class="kp">&amp;</span><span class="o">'</span><span class="na">a</span> <span class="nc">mut</span><span class="w"> </span><span class="kt">u32</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">    </span><span class="n">a</span><span class="p">.</span><span class="n">max</span><span class="p">(</span><span class="n">b</span><span class="p">)</span><span class="w"></span>
<span class="p">}</span><span class="w"></span>
</code></pre></div>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>